l:IdLnk, dt:fpf(Id; tg.Type), tg:Id.
sqequal(fpf-dom(Kind-deq; rcv(l,tg); lnk-decl(l; dt)); fpf-dom(id-deq; tg; dt)) 

latex

Definitions	deq-member(eq; x; L), , t  T, guard(T), P  Q, x:A. B(x), sq_type(T), fpf-dom(eq; x; f), lnk-decl(l; dt), fpf(A; a.B(a)), IdLnk, Id, x. t(x), P  Q, x:A. B(x), (x  l), Knd, rcv(l,tg), P  Q, P  Q, map(f; as), Kind-deq, id-deq, b, prop{i:l}
Lemmas	l member wf, rcv one one, Id sq, iff imp equal bool, assert wf, deq-member wf, assert-deq-member, id-deq wf, Kind-deq wf, map wf, member map, Knd wf, rcv wf, fpf wf, Id wf, IdLnk wf, bool sq